\begin{tabbing}
$\forall$${\it es}$:ES, $A$:Type, $X$:AbsInterface($A$ List), $e$:E.
\\[0ex]($\neg$($\uparrow$first($e$)))
\\[0ex]$\Rightarrow$ (\=es{-}interface{-}history(${\it es}$;$X$;$e$)\+
\\[0ex]=
\\[0ex]if $e$ $\in_{b}$ $X$
\\[0ex]then es{-}interface{-}history(${\it es}$;$X$;pred($e$)) @ $X$($e$)
\\[0ex]else es{-}interface{-}history(${\it es}$;$X$;pred($e$))
\\[0ex]fi 
\\[0ex]$\in$ ($A$ List))
\-
\end{tabbing}